fix(abi): type-check all 17 Idris2 proofs under 0.8.0#189
Merged
Conversation
Six ABI modules never compiled against the pinned Idris2 0.8.0 toolchain,
and the package build never exercised them: `just typecheck` used an
invalid `--check --package boj boj.ipkg` invocation, and CartridgeDispatch
+ APIContractCoverage were absent from boj.ipkg. Theorem statements and the
axiom budget are unchanged — only the proofs' construction.
- CartridgeDispatch: 0.8.0 with-clause syntax (full LHS / `_ |`); dispatch
factored through a reducible helper so refused-completeness is provable;
conjunction + Uninhabited lemmas replace unsound `absurd` shortcuts.
- SafePromptInjection, SafeCORS: with-abstraction rewrites the goal to
True = True, so the residual obligations are Refl.
- SafeHTTP: add Data.List.Elem/Data.Maybe imports; IsJust -> isJust;
all -> allRec (to match the SafetyLemmas lemmas); explicit {xs,ys}
binders (auto-generalised implicits are erased); fix let-annotation parse.
- SafeWebSocket: FrameSizeSafe is now FrameSizeSafeUpTo maxFrameSize over a
bound-parameterised family — baking the 16 MiB literal into a constructor
LTE index forced a unary Nat and exhausted the elaborator.
- APIContractCoverage: qualify representativeCatalogue (was auto-bound as a
fresh implicit, shadowing the global).
- SafetyLemmas: add constructive lemma `allTake`. No new axioms.
Plumbing: fix `just typecheck` to use `--typecheck <pkg>.ipkg`; add the two
missing modules to boj.ipkg; reconcile `verify-no-believe-me` to the
sanctioned 5-axiom trusted base. Docs updated (PROOF-NEEDS.md, proofs
README).
All 17 modules build clean; believe_me count = 5 (documented class-(J)).
https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa
🏁 path-claims benchCommit NumbersHost-dependent — compare deltas across commits, not absolute values. |
🔍 Hypatia Security ScanFindings: 255 issues detected
View findings[
{
"reason": "Stale AI session file -- delete",
"type": "stale",
"file": "GEMINI.md",
"action": "delete",
"rule_module": "root_hygiene",
"severity": "medium"
},
{
"reason": "Action if: always()\n uses: actions/upload-artifact@ea165 needs attention",
"type": "unpinned_action",
"file": "e2e.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in abi-drift.yml",
"type": "missing_timeout_minutes",
"file": "abi-drift.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in container-publish.yml",
"type": "missing_timeout_minutes",
"file": "container-publish.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
marked this pull request as ready for review
June 3, 2026 19:32
hyperpolymath
enabled auto-merge (squash)
June 3, 2026 19:32
hyperpolymath
disabled auto-merge
June 3, 2026 23:37
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Against the pinned toolchain (Idris2 0.8.0, Chez backend), 6 of the 17 core ABI proof modules did not type-check — yet all were marked "✅ Complete". They rotted undetected because the build never exercised them:
just typecheckused an invalid invocation (idris2 --check --package boj boj.ipkg→ "Can't find package boj"); the correct form is--typecheck boj.ipkg.CartridgeDispatchandAPIContractCoveragewere absent fromboj.ipkg, so the package build skipped them entirely.After this PR,
cd src/abi && idris2 --typecheck boj.ipkgbuilds all 17 modules clean. Theorem statements and the axiom budget are unchanged — the fixes are in the proofs' construction.Proof fixes (all constructive, zero new axioms)
CartridgeDispatchwithsyntax 0.8.0 rejects;refusedIfNoMatchneeded a reducibledispatch;absurdlackedUninhabitedinstanceswith;dispatchvia reducibledispatchOnhelper; conjunction +statusEqSoundReady+ 3UninhabitedlemmasSafePromptInjectionwith-abstraction rewrites goal toTrue = TrueRight ReflSafeCORSwithissue; undefinedfromLteTrue(Refl, Refl);fromLteTrue→lteReflectsLTESafeHTTPData.List.Elem/Data.Maybe;IsJust→isJust;all→allRec; erased implicits;let x : a = bmis-parse{xs,ys}, parenthesised annotationsSafeWebSocketmaxFrameSizebaked into a constructorLTEindex forced a unaryNatFrameSizeSafeUpTo;FrameSizeSafe/ControlFrameSizeSafebecome synonymsAPIContractCoveragerepresentativeCatalogueauto-bound as a fresh implicit (shadowed the global)SafetyLemmasallTakereferenced but undefinedPlumbing & docs
boj.ipkg: addedBoj.CartridgeDispatch+Boj.APIContractCoverage.Justfile:typechecknow uses--typecheck;verify-no-believe-mereconciled to the sanctioned 5-axiom trusted base (it previously enforced zero, contradictingPROOF-NEEDS.md), and fails on any otherbelieve_meor on axiom-count drift.PROOF-NEEDS.md/verification/proofs/README.adoc: build-verification notes.Trusted base unchanged
believe_mecount = 5, all inSafetyLemmas.idr, all%unsafeclass-(J) axioms (opaqueChar/Stringprimitives). Noassert_total/assert_smaller/ new%unsafeanywhere.Roadmap (this branch, follow-up commits)
bojABI package green under 0.8.0.idrfiles)Draft until the cartridge ABIs are also green.
https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa
Generated by Claude Code